(set-logic QF_LIA)
(set-info :source |http://www.nec-labs.com/~fsoft/bench.html
 The following changes have been made:
 The logic is changed to QF_LIA.
 The category is set as industrial.
 The status (except 'large' cases) is assigned according to the 'outfile' on http://www.nec-labs.com/~fsoft/bench.html.  |)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun i194 () Int)
(declare-fun i201 () Int)
(declare-fun i224 () Int)
(declare-fun i214 () Int)
(declare-fun i245 () Int)
(declare-fun i270 () Int)
(declare-fun i300 () Int)
(declare-fun i342 () Int)
(declare-fun i399 () Int)
(declare-fun i481 () Int)
(declare-fun i527 () Int)
(declare-fun i578 () Int)
(assert (let ((?v_3 (+ 0 0))) (let ((?v_74 (= i399 ?v_3))) (let ((?v_75 (ite ?v_74 1 2147483647)) (?v_0 (ite (<= i194 ?v_3) 4 12)) (?v_42 (+ 12 0))) (let ((?v_2 (= ?v_0 ?v_42))) (let ((?v_51 (ite (not ?v_2) 0 i201)) (?v_1 (ite ?v_2 14 ?v_0))) (let ((?v_4 (= ?v_51 ?v_3)) (?v_49 (+ 14 0))) (let ((?v_5 (ite (not (= ?v_1 ?v_49)) ?v_1 (ite (not ?v_4) 15 (ite ?v_4 16 ?v_1)))) (?v_68 (+ 16 0))) (let ((?v_13 (= ?v_5 ?v_68)) (?v_67 (+ 15 0))) (let ((?v_12 (= ?v_5 ?v_67))) (let ((?v_6 (ite ?v_12 17 (ite ?v_13 17 ?v_5))) (?v_78 (+ 17 0))) (let ((?v_8 (= ?v_6 ?v_78))) (let ((?v_91 (ite (not ?v_8) 0 i224)) (?v_7 (ite ?v_8 19 ?v_6))) (let ((?v_9 (= ?v_91 ?v_3)) (?v_89 (+ 19 0))) (let ((?v_10 (ite (not (= ?v_7 ?v_89)) ?v_7 (ite (not ?v_9) 20 (ite ?v_9 21 ?v_7)))) (?v_109 (+ 21 0))) (let ((?v_15 (= ?v_10 ?v_109)) (?v_107 (+ 20 0))) (let ((?v_14 (= ?v_10 ?v_107))) (let ((?v_11 (ite ?v_14 23 (ite ?v_15 23 ?v_10))) (?v_16 (<= (ite ?v_12 i214 (ite (not ?v_13) 0 i214)) (+ (ite ?v_14 i245 (ite (not ?v_15) 0 i245)) 0)))) (let ((?v_17 (ite (not (= ?v_11 (+ 23 0))) ?v_11 (ite (not ?v_16) 24 (ite ?v_16 56 ?v_11)))) (?v_31 (+ 56 0))) (let ((?v_21 (= ?v_17 ?v_31)) (?v_18 (= ?v_17 (+ 24 0)))) (let ((?v_35 (ite (not ?v_21) 0 i270)) (?v_19 (= (ite (not ?v_18) 0 i270) ?v_3))) (let ((?v_22 (= ?v_35 ?v_3)) (?v_20 (ite ?v_18 26 (ite ?v_21 58 ?v_17))) (?v_33 (+ 58 0))) (let ((?v_23 (ite (= ?v_20 (+ 26 0)) (ite (not ?v_19) 27 (ite ?v_19 28 ?v_20)) (ite (not (= ?v_20 ?v_33)) ?v_20 (ite (not ?v_22) 59 (ite ?v_22 60 ?v_20))))) (?v_45 (+ 60 0))) (let ((?v_29 (= ?v_23 ?v_45)) (?v_44 (+ 59 0))) (let ((?v_28 (= ?v_23 ?v_44)) (?v_25 (= ?v_23 (+ 28 0))) (?v_24 (= ?v_23 (+ 27 0)))) (let ((?v_57 (ite ?v_28 i300 (ite (not ?v_29) 0 i300))) (?v_26 (<= (ite ?v_24 i300 (ite (not ?v_25) 0 i300)) ?v_3))) (let ((?v_30 (<= ?v_57 ?v_3)) (?v_27 (ite ?v_24 30 (ite ?v_25 30 (ite ?v_28 62 (ite ?v_29 62 ?v_23))))) (?v_54 (+ 62 0))) (let ((?v_32 (ite (= ?v_27 (+ 30 0)) (ite ?v_26 56 (ite (not ?v_26) 46 ?v_27)) (ite (not (= ?v_27 ?v_54)) ?v_27 (ite (not ?v_30) 63 (ite ?v_30 69 ?v_27)))))) (let ((?v_41 (= ?v_32 (+ 46 0))) (?v_70 (+ 69 0))) (let ((?v_40 (= ?v_32 ?v_70)) (?v_69 (+ 63 0))) (let ((?v_38 (= ?v_32 ?v_69)) (?v_34 (= ?v_32 ?v_31))) (let ((?v_82 (ite (not ?v_38) 0 i342)) (?v_36 (= (ite (not ?v_34) ?v_35 i342) ?v_3))) (let ((?v_39 (= ?v_82 ?v_3)) (?v_47 (ite ?v_40 9 (ite (not ?v_41) 0 i342))) (?v_37 (ite ?v_34 58 (ite ?v_38 65 (ite ?v_40 74 (ite ?v_41 48 ?v_32))))) (?v_84 (+ 74 0))) (let ((?v_46 (= ?v_37 ?v_84)) (?v_80 (+ 65 0))) (let ((?v_64 (ite (not ?v_46) 0 ?v_47))) (let ((?v_65 (<= 9 (+ ?v_64 0))) (?v_99 (+ 264 0))) (let ((?v_48 (<= ?v_64 ?v_99)) (?v_43 (ite (= ?v_37 ?v_33) (ite (not ?v_36) 59 (ite ?v_36 60 ?v_37)) (ite (= ?v_37 ?v_80) (ite (not ?v_39) 66 (ite ?v_39 67 ?v_37)) (ite ?v_46 97 (ite (not (= ?v_37 (+ 48 0))) ?v_37 (ite (not (<= ?v_47 ?v_3)) 12 ?v_37)))))) (?v_96 (+ 97 0)) (?v_95 (+ 67 0))) (let ((?v_60 (= ?v_43 ?v_95)) (?v_94 (+ 66 0))) (let ((?v_59 (= ?v_43 ?v_94)) (?v_56 (= ?v_43 ?v_45)) (?v_55 (= ?v_43 ?v_44)) (?v_50 (= ?v_43 ?v_42)) (?v_61 (not ?v_60))) (let ((?v_52 (= (ite (not ?v_50) ?v_51 i399) ?v_3)) (?v_76 (ite ?v_59 i399 (ite ?v_61 0 i399))) (?v_58 (<= (ite ?v_55 i399 (ite (not ?v_56) ?v_57 i399)) ?v_3))) (let ((?v_77 (<= (ite ?v_59 ?v_75 (ite ?v_61 0 ?v_75)) (+ ?v_76 0))) (?v_53 (ite ?v_50 14 (ite ?v_55 62 (ite ?v_56 62 (ite ?v_59 93 (ite ?v_60 93 (ite (not (= ?v_43 ?v_96)) ?v_43 (ite (not ?v_48) 98 (ite ?v_48 95 ?v_43))))))))) (?v_71 (+ 95 0)) (?v_122 (+ 98 0)) (?v_115 (+ 93 0)) (?v_72 (not ?v_65)) (?v_88 (+ 76 0)) (?v_87 (+ 96 0)) (?v_85 (+ 91 0)) (?v_132 (+ 94 0))) (let ((?v_86 (not ?v_77)) (?v_103 (+ 82 0)) (?v_102 (+ 77 0)) (?v_101 (+ 92 0)) (?v_125 (+ 101 0)) (?v_62 (ite ?v_74 0 (- 2147483647)))) (let ((?v_119 (ite ?v_59 ?v_62 (ite ?v_61 0 ?v_62)))) (let ((?v_63 (<= ?v_76 (+ ?v_119 0)))) (let ((?v_66 (ite (= ?v_53 ?v_49) (ite (not ?v_52) 15 (ite ?v_52 16 ?v_53)) (ite (= ?v_53 ?v_54) (ite (not ?v_58) 63 (ite ?v_58 69 ?v_53)) (ite (= ?v_53 ?v_115) (ite (not ?v_63) 94 (ite ?v_63 91 ?v_53)) (ite (= ?v_53 ?v_122) 95 (ite (not (= ?v_53 ?v_71)) ?v_53 (ite ?v_72 96 (ite ?v_65 76 ?v_53))))))))) (let ((?v_73 (= ?v_66 ?v_132)) (?v_81 (= ?v_66 ?v_69)) (?v_98 (= ?v_66 ?v_70))) (let ((?v_79 (ite (= ?v_66 ?v_67) 17 (ite (= ?v_66 ?v_68) 17 (ite ?v_81 65 (ite ?v_98 74 (ite (= ?v_66 ?v_71) (ite ?v_72 96 (ite ?v_65 76 ?v_66)) (ite ?v_73 91 (ite (= ?v_66 ?v_85) (ite ?v_86 92 (ite ?v_77 69 ?v_66)) (ite (= ?v_66 ?v_87) 76 (ite (= ?v_66 ?v_88) 77 ?v_66))))))))))) (let ((?v_90 (= ?v_79 ?v_78)) (?v_111 (= ?v_79 ?v_70)) (?v_83 (= (ite (not ?v_81) ?v_82 i481) ?v_3)) (?v_97 (= ?v_79 ?v_84)) (?v_104 (= ?v_79 ?v_102)) (?v_112 (= ?v_79 ?v_103))) (let ((?v_93 (ite ?v_90 19 (ite ?v_111 74 (ite (= ?v_79 ?v_80) (ite (not ?v_83) 66 (ite ?v_83 67 ?v_79)) (ite ?v_97 97 (ite (= ?v_79 ?v_85) (ite ?v_86 92 (ite ?v_77 69 ?v_79)) (ite (= ?v_79 ?v_87) 76 (ite (= ?v_79 ?v_88) 77 (ite (= ?v_79 ?v_101) 69 (ite ?v_104 101 (ite ?v_112 74 ?v_79))))))))))) (?v_92 (= (ite (not ?v_90) ?v_91 i527) ?v_3))) (let ((?v_110 (= ?v_93 ?v_84)) (?v_116 (= ?v_93 ?v_94)) (?v_117 (= ?v_93 ?v_95)) (?v_105 (ite ?v_98 9 ?v_47))) (let ((?v_113 (ite (not ?v_97) ?v_64 ?v_105))) (let ((?v_100 (<= ?v_113 ?v_99)) (?v_126 (= ?v_93 ?v_102)) (?v_128 (ite (not ?v_104) 0 ?v_105))) (let ((?v_106 (<= ?v_128 ?v_99))) (let ((?v_108 (ite (= ?v_93 ?v_89) (ite (not ?v_92) 20 (ite ?v_92 21 ?v_93)) (ite (= ?v_93 ?v_70) 74 (ite ?v_110 97 (ite ?v_116 93 (ite ?v_117 93 (ite (= ?v_93 ?v_96) (ite (not ?v_100) 98 (ite ?v_100 95 ?v_93)) (ite (= ?v_93 ?v_88) 77 (ite (= ?v_93 ?v_101) 69 (ite ?v_126 101 (ite (= ?v_93 ?v_103) 74 (ite (not (= ?v_93 ?v_125)) ?v_93 (ite (not ?v_106) 102 (ite ?v_106 99 ?v_93)))))))))))))) (?v_118 (not ?v_117)) (?v_120 (ite (= i578 ?v_3) 0 (- 2147483647)))) (let ((?v_121 (<= (ite ?v_116 i578 (ite ?v_118 ?v_76 i578)) (+ (ite ?v_116 ?v_120 (ite ?v_118 ?v_119 ?v_120)) 0))) (?v_127 (ite ?v_111 9 (ite (not ?v_112) ?v_105 (+ 0 1 ?v_105))))) (let ((?v_123 (ite ?v_110 ?v_127 ?v_113))) (let ((?v_114 (<= ?v_123 ?v_99)) (?v_124 (<= 9 (+ ?v_123 0))) (?v_130 (ite ?v_126 ?v_127 ?v_128))) (let ((?v_129 (<= ?v_130 ?v_99)) (?v_131 (<= 9 (+ ?v_130 0)))) (and (and true (not ?v_73)) (= (ite (= ?v_108 ?v_107) 23 (ite (= ?v_108 ?v_109) 23 (ite (= ?v_108 ?v_70) 74 (ite (= ?v_108 ?v_84) 97 (ite (= ?v_108 ?v_96) (ite (not ?v_114) 98 (ite ?v_114 95 ?v_108)) (ite (= ?v_108 ?v_115) (ite (not ?v_121) 94 (ite ?v_121 91 ?v_108)) (ite (= ?v_108 ?v_122) 95 (ite (= ?v_108 ?v_71) (ite (not ?v_124) 96 (ite ?v_124 76 ?v_108)) (ite (= ?v_108 ?v_102) 101 (ite (= ?v_108 ?v_103) 74 (ite (= ?v_108 ?v_125) (ite (not ?v_129) 102 (ite ?v_129 99 ?v_108)) (ite (= ?v_108 (+ 102 0)) 99 (ite (not (= ?v_108 (+ 99 0))) ?v_108 (ite (not ?v_131) 100 (ite ?v_131 79 ?v_108))))))))))))))) ?v_132))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(exit)
